op { graph_op_name: "While" visibility: HIDDEN }
